S1: Functional Choreographies with Pirouette
Pirouette is a higher-order, typed functional choreographic programming language. Pirouette lets developers design distributed systems as centralized functional programs, which are then automatically compiled into distributed implementations for each participant via endpoint projection. The language’s enables choreographies to be passed as program values, embracing abstraction and reuse.
Goals
First, become familiar Pirouette, write small choreographic programs using the Pirouette-Compiler.
Then, you could either explore the paper describing First-Class Location (Set) Polymorphism as an extension, or compare Pirouette with a choreographic programming library, like MultiChor.
Starting Points
- Paper Pirouette: Higher-Order Typed Functional Choreographies
- Pirouette Compiler (in OCaml)
- Pirouette Proofs Zenodo, or
- Pirouette Proofs Gitlab, or